<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
  <head>
    <title>Package alloy.transform Documentation</title>
  </head>

  <body>
    <p>This package contains classes which perform various desugarings
      on an Alloy AST, resulting in a formula(s) which can be translated
      into a boolean formula for analysis.  All classes in this
      package assume that the AST they operate on corresponds to a
      semantically correct Alloy model.  In particular, {@link
      alloy.AlloyRunner#_performElaborations}, which uses the classes
      in this package, is run after {@link
      alloy.AlloyRunner#_performSemanticChecks}, which ensures the
      spec is semantically correct.
      <p>Here is a high-level overview of the classes in this package.
      <ul>
      <li>{@link DesugarOverrideVisitor}: desugars the ++ operator.
      <li>Inline invocations.  This happens using the following steps:
	<ul><li>Construct a graph (should be a DAG) whose nodes are
	    functions and whose edges indicate invocations of one
	    function by another using {@link
	    alloy.transform.ConstructInvocationGraphVisitor}.  This is
	    done to check that there are no recursive invocations,
	    since we do not currently support this feature.
	    Eventually, this check may be removed or modified.


	<li>Inline invocations in the body of functions by calling
	{@link
	alloy.transform.InvocationInlineVisitor#inlineFunctionBodyInvocations}
	with a topologically sorted list of functions obtained from
		the visitor applied in the previous step.
	<li>Finally, inline the remaining invocations in facts and
	    assertions by applying an {@link
	    alloy.transform.InvocationInlineVisitor}.  Inlining
	    an invocation may involve replacing formals in the
	    function body with actual parameters and replacing var types in the
	    function body with the basic types implied by the
	    invocation, which is accomplished with the help of a
	    {@link alloy.transform.FormalAndTypeReplaceVisitor}.</ul>

	Note that we do not currently check invocation arguments to
	see if they meet the constraints implied by qualifiers and
	multiplicity markings in the formal declarations of the
	arguments.  Also note that inlining an invocation can generate
	new basic types.
      <li>Check scopes for commands and generate dummy types for
	polymorphic assertions and functions using a 
	{@link alloy.semantic.CommandVisitor} (for example, in
	checking assert [t] { ... }, generates a new dummy type for
	t).  Note that this visitor is currently broken when we have
	multiple commands and one of them requires dummy types because
	dummy types get added to global state.
      <li>Finally, generate a formula for each command by applying a
	{@link alloy.transform.GenCommandFormulasVisitor}.  This
	visitor performs the following steps:
	<ul><li>Generates the formula for only the paragraph specified
	    in the command using a 
            {@link alloy.transform.GenBasicCommandFormulasVisitor}.
	    This visitor also handles replacing VarTypes of type
	    parameters of paragraphs with previously generated dummy
	    types using a {@link
	    alloy.transform.FormalAndTypeReplaceVisitor}.  Note that
	    this pass can result in the generation of new basic types.
	    For example, when checking assert [t] { all A[t] | ... },
	    A will be instantiated with the dummy type for t to create
	    a new basic type.
	    <li>Instantiates polymorphic facts using a {@link
	    alloy.transform.PolymorphicFactVisitor}, which in turn
	    uses {@link alloy.transform.FormalAndTypeReplaceVisitor}'s
	    to change types in the polymorphic facts as needed.  Note
	    that <em>no</em> new basic types are created by this
	    visitor.
	    <li>Generate formulas for implicit constraints from
	    multiplicities and qualifiers in signature declarations by
	    calling {@link
	    alloy.transform.TypeConstraints#createTypeConstraints}.
	    This method should only be run after all basic types for
	    this command have been created because it iterates through
	    the global list of BasicType's and creates constraints for
	    each of them.  Note that this method also creates leaf ids
	    for all basic types.
	    <li>Construct a "mega-fact" which is a conjoining of all
	    facts and declaration constraints from signatures by
	    applying a {@link alloy.transform.MegaFactVisitor}.  Note
	    that the formulas for all commands refer to the same
	    mega-fact formula object.  
	    <li>Finally, for each command do the following:
	    <ul><li>If the command is a "check" command, negate its
		formula.  If the command is a "run" command and its
		function has arguments, existentially quantify the
		arguments over the formula.
		<li>Conjoin the mega-fact to the formula of the command.
		<li>Desugar all quantifiers in the formula by
		applying a {@link
		alloy.transform.DesugarQuantifiersVisitor}.  
		<li>Create constraints implied by qualifiers and
		multiplicities in declarations of quantified formulas
		by applying a {@link
		alloy.transform.DesugarDeclsVisitor}.  Note that this
		does not yet create constraints for declarations in
		the "sum" construct.  Note that a {@link
		alloy.transform.DesugarQuantifiersVisitor} is again
		applied <em>after</em> this pass, since the constraints implied
		by declarations sometimes introduce new quantifiers
		(ie., all x: option A | f goes to all x: A | sole x =>
		f, and then "sole x" needs to be desugared to # x =<
		1.
		<li>Perform miscellaneous AST simplifications by
		applying a {@link alloy.transform.SimplifyVisitor}.
		<li>Set leaf ids of all leaves in the AST by applying
		a {@link alloy.transform.SetLeafIdsVisitor}.
		<li>Perform skolemization on the formula by running
		{@link
		alloy.transform.SkolemizationVisitor#skolemize}.  Note
		that this method returns a formula containing
		constraints for any generated skolem constants, which
		is then conjoined to the formula for the command
		without negation.
		<li>Finally, desugar the let construct by applying a
		{@link alloy.transform.DesugarLetVisitor}.  Note that
		we need to add correct support for a real "let"
		construct.</ul>
	    </ul></ul>
		
	    


<!-- Created: Fri Sep
	14 08:52:03 edt 2001 --> <!-- hhmts start --> Last modified:
	Fri Sep 14 09:03:17 edt 2001 <!-- hhmts end -->
  </body>
</html>
